import atom.UnaryAtom;
import formula.BinaryFormula;
import formula.Formula;
import formula.UnaryFormula;
import literal.UnaryLiteral;
import proof.ConclusionProof;
import proof.Proof;
import sign.FormulaSign;

import java.util.ArrayList;
import java.util.Random;

public class GenerateFormulas {
    public ArrayList<String> getElement(){
        String[] alphabet={"a","b","c","d","e","f","g","h","i","j","k","l","m","n",
                "o","p","q","r","s","t","u","v","w","x","y","z"};
        ArrayList<String> arr=new ArrayList<>();
        for (int i = 0; i < 4; i++) {//在alphabet中挑选5个字母作为初始输入
            Random random=new Random();
            int randomInt=random.nextInt(26);
            String atom=alphabet[randomInt];
            arr.add(atom);
        }
//        for (String str:arr) {
//            System.out.println(str);
//        }
        return arr;
    }

    public BinaryFormula GenerateFormula(ArrayList<String> arr){
        UnaryFormula uf1=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(0)),false));
        UnaryFormula uf2=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(1)),false));
        UnaryFormula uf3=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(2)),false));
        UnaryFormula uf4=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(3)),false));
        //UnaryFormula uf5=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(4)),false));
        ArrayList<UnaryFormula> ufArr=new ArrayList<>();
        ufArr.add(uf1);
        ufArr.add(uf2);
        ufArr.add(uf3);
        ufArr.add(uf4);
        //ufArr.add(uf5);

        Random randomS=new Random();
        int sign=randomS.nextInt(2);//random sign
        Random randomT=new Random();
        int type=randomT.nextInt(2);//random type(bf/tf)

        Random random=new Random();
        int e1=random.nextInt(4);//从5个初始element中选择，与getelement中的i值对应
        int e2=random.nextInt(4);
        int e3=random.nextInt(4);

        if (type==0){//bf
            if (sign==0){
                //System.out.println("exist");
                BinaryFormula bf=new BinaryFormula(FormulaSign.EXIST,ufArr.get(e1),ufArr.get(e2));
               return bf;
            }else{
                //System.out.println("any");
                BinaryFormula bf=new BinaryFormula(FormulaSign.ANY,ufArr.get(e1),ufArr.get(e2));
               return bf;
            }
        }else {//tf
            Random randomS2=new Random();
            int sign2=randomS2.nextInt(2);//random sign(inner one)
            if (sign==0){//outer sign is exist
                if (sign2==0){//inner sign is exist
                    //total formula is (E,E)
                    BinaryFormula bfInner=new BinaryFormula(FormulaSign.EXIST,ufArr.get(e2),ufArr.get(e3));
                    BinaryFormula bf=new BinaryFormula(FormulaSign.EXIST,ufArr.get(e1),bfInner);
                    return bf;
                }else{//inner sign is for any
                    //total formula is (E,A)
                    BinaryFormula bfInner=new BinaryFormula(FormulaSign.ANY,ufArr.get(e2),ufArr.get(e3));
                    BinaryFormula bf=new BinaryFormula(FormulaSign.EXIST,ufArr.get(e1),bfInner);
                   return bf;
                }
            }else {//outer sign is for all
                if (sign2==0){//inner sign is exist
                    //total formula is (A,E)
                    BinaryFormula bfInner=new BinaryFormula(FormulaSign.EXIST,ufArr.get(e2),ufArr.get(e3));
                    BinaryFormula bf=new BinaryFormula(FormulaSign.ANY,ufArr.get(e1),bfInner);
                    return bf;
                }else{//inner sign is for any
                    //total formula is (A,A)
                    BinaryFormula bfInner=new BinaryFormula(FormulaSign.ANY,ufArr.get(e2),ufArr.get(e3));
                    BinaryFormula bf=new BinaryFormula(FormulaSign.ANY,ufArr.get(e1),bfInner);
                    return bf;
                }
            }
        }
    }

    public ArrayList<BinaryFormula> getFormulas(int i,ArrayList<String> arr){
        ArrayList<BinaryFormula> conditions=new ArrayList<>();
        for (int j = 0; j < i; j++) {
            BinaryFormula bf=GenerateFormula(arr);
            conditions.add(bf);
        }
        return conditions;
    }

    public BinaryFormula getConclusion(ArrayList<String> arr){
        BinaryFormula bf=GenerateFormula(arr);
        return bf;
    }

    public void run(){

//        long startTime = System.currentTimeMillis(); // 记录开始时间
        GenerateFormulas gen=new GenerateFormulas();
        ArrayList<String> eleArr=gen.getElement();
        ArrayList<BinaryFormula> conditions=gen.getFormulas(3,eleArr);
        BinaryFormula conclusion= gen.getConclusion(eleArr);


        ArrayList<Proof> proofs=new ArrayList<>();
        Proof p1=new ConclusionProof(conditions.get(0));
        Proof p2=new ConclusionProof(conditions.get(1));
        Proof p3=new ConclusionProof(conditions.get(2));
        //Proof p4=new ConclusionProof(conditions.get(3));
        //Proof p5=new ConclusionProof(conditions.get(4));
        proofs.add(p1);
        proofs.add(p2);
        proofs.add(p3);
        //proofs.add(p4);
        //proofs.add(p5);
        if (Solve.solveHelper(proofs,conclusion, new UsedCondition())!=null){
            System.out.println("  ");
            for (BinaryFormula bf:conditions) {
                System.out.println(bf);
            }
            System.out.println(conclusion);

            System.out.println(Solve.solveHelper(proofs,conclusion, new UsedCondition()));
//            long endTime = System.currentTimeMillis(); // 记录结束时间
//            long duration = endTime - startTime; // 计算时间（毫秒）
//           System.out.println("running time is: " + duration + " ms");
        }

    }

    public static void main(String[] args) {
        GenerateFormulas gf=new GenerateFormulas();
        for (int i=0;i<50;i++){
            gf.run();
        }
        System.out.println("done");

    }
}
